Boolean Satisfiability (SAT) is arguably the archetypical NP-completedecision problem. Progress in SAT solving algorithms has motivated an everincreasing number of practical applications in recent years. However, manypractical uses of SAT involve solving function as opposed to decision problems.Concrete examples include computing minimal unsatisfiable subsets, minimalcorrection subsets, prime implicates and implicants, minimal models, backboneliterals, and autarkies, among several others. In most cases, solving afunction problem requires a number of adaptive or non-adaptive calls to a SATsolver. Given the computational complexity of SAT, it is therefore important todevelop algorithms that either require the smallest possible number of calls tothe SAT solver, or that involve simpler instances. This paper addresses anumber of representative function problems defined on Boolean formulas, andshows that all these function problems can be reduced to a generic problem ofcomputing a minimal set subject to a monotone predicate. This problem isreferred to as the Minimal Set over Monotone Predicate (MSMP) problem. Thisexercise provides new ways for solving well-known function problems, includingprime implicates, minimal correction subsets, backbone literals, independentvariables and autarkies, among several others. Moreover, this exercisemotivates the development of more efficient algorithms for the MSMP problem.Finally the paper outlines a number of areas of future research related withextensions of the MSMP problem.
展开▼
